package driver;

import java.io.File;
import java.io.FileNotFoundException;

import java.util.Map;
import java.util.HashMap;

import graph.GraphFactory;
import graph.Graph;
import graph.State;

import ndfs.nndfs.Color;

import ndfs.NDFS;
import ndfs.NDFSFactory;
import ndfs.Result;

public class Main {

	private static class ArgumentException extends Exception {
		private static final long serialVersionUID = 1L;

		ArgumentException(String message) {
			super(message);
		}
	};

	private static void printUsage() {
		System.out.println("Usage: bin/ndfs <file> <version> <nrWorkers>");
		System.out.println("  where");
		System.out.println("    <file> is a Promela file (.prom)");
		System.out.println("    <version> is one of {seq, par}");
	}

	private static void runNDFS(String version, Map<State, ndfs.nndfs.Color> colorStore,
			File file) throws FileNotFoundException {

		Graph graph = GraphFactory.createGraph(file);
		NDFS ndfs = NDFSFactory.createNNDFS(graph, colorStore);
		long start = System.currentTimeMillis();
		long end;
		try {
			ndfs.ndfs();
			throw new Error("No result returned by " + version);
		} catch (Result r) {
			end = System.currentTimeMillis();
			System.out.println(r.getMessage());
			System.out.printf("%s took %d ms\n", version, end - start);
		}
	}
	
	private static void runMCNDFS(int thread, Map<State, ndfs.mcndfs_1_naive.Color> colorStore, File file, Map<graph.State, Boolean> redMap, Map<graph.State, Integer> counterMap) {
		Graph graph = null;
		try {
			graph = GraphFactory.createGraph(file);
		} catch (FileNotFoundException e) {
			System.err.println(e.getMessage());
			return;
		}
		NDFS ndfs = NDFSFactory.createMCNDFSNaive(graph, colorStore, redMap, counterMap);
		ndfs.setThreadId(thread);
		long start = System.currentTimeMillis();
		long end;
		try {
			ndfs.ndfs();
			throw new Error("No result returned by thread " + thread);
		} catch (Result r) {
			end = System.currentTimeMillis();
			System.out.println(r.getMessage());
			System.out.printf("Thread %s took %d ms\n", thread, end - start);
			// Either no cycle has been found or a cycle has been found, kill all threads.
			for (Thread t : threads) {
				if (t != Thread.currentThread() && t.isAlive()) {
					// Don't kill itself, would interrupt killing process
					t.stop();
				}
			}
		}
	}
	
	static NDFSThread[] threads;

	private static void dispatch(final File file, String version, int nrWorkers)
			throws ArgumentException, FileNotFoundException {
		if (version.equals("seq")) {
			if (nrWorkers != 1) {
				throw new ArgumentException("seq can only run with 1 worker");
			}
			Map<State, ndfs.nndfs.Color> map = new HashMap<State, ndfs.nndfs.Color>();
			runNDFS("seq", map, file);
		} else if (version.equals("par")){
			threads = new NDFSThread[nrWorkers];
			// Multi-core parallel NDFS
			if (nrWorkers < 2) {
				throw new ArgumentException("par can only run with more than 1 worker");
			}
			// Initialize global maps
			Map<State, Boolean> redMap = new HashMap<State, Boolean>();
			Map<State, Integer> counterMap = new HashMap<State, Integer>();
			for (int i = 0; i < nrWorkers; i++) {
				NDFSThread t = new Main().new NDFSThread(file, i, redMap, counterMap);
				t.start();
				threads[i] = t;
			}
		} else {
			throw new ArgumentException("Unkown version: " + version);
		}
	}
	
	private class NDFSThread extends Thread {
		private File file;
		private int threadID;
		private Map<graph.State, Boolean> redMap;
		private Map<graph.State, Integer> counterMap;
		
		public NDFSThread (File file, int thread, Map<graph.State, Boolean> redMap, Map<graph.State, Integer> counterMap) {
			this.file = file;
			this.threadID = thread;
			this.redMap = redMap;
			this.counterMap = counterMap;
		}
		
		public void run() {
			Map<graph.State, ndfs.mcndfs_1_naive.Color> map = new HashMap<graph.State, ndfs.mcndfs_1_naive.Color>();
			runMCNDFS(threadID, map, file, redMap, counterMap);
		}
	}

	public static void main(String[] argv) {
		try {
			if (argv.length != 3)
				throw new ArgumentException("Wrong number of arguments");
			File file = new File(argv[0]);
			String version = argv[1];
			int nrWorkers = new Integer(argv[2]);

			dispatch(file, version, nrWorkers);
		} catch (FileNotFoundException e) {
			System.err.println(e.getMessage());
		} catch (ArgumentException e) {
			System.err.println(e.getMessage());
			printUsage();
		} catch (NumberFormatException e) {
			System.err.println(e.getMessage());
			printUsage();
		}
	}
}
